\begin{tabbing}
$\forall$$T$:Type, ${\it as}$, ${\it bs}$:$T$ List.
\\[0ex]no\_repeats($T$;${\it as}$)
\\[0ex]$\Rightarrow$ no\_repeats($T$;${\it bs}$)
\\[0ex]$\Rightarrow$ (\=${\it as}$ $=$ ${\it bs}$\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($\forall$$x$:$T$. ($x$ $\in$ ${\it as}$) $\Leftrightarrow$ ($x$ $\in$ ${\it bs}$)) \& ($\forall$$x$, $y$:$T$. $x$ before $y$ $\in$ ${\it as}$ $\Leftrightarrow$ $x$ before $y$ $\in$ ${\it bs}$))
\-
\end{tabbing}